TypeNames:Type, d:DS(TypeNames), a:TypeNames.
dseq(d;a)  dstype(TypeNames; d; a)dstype(TypeNames; d; a) 

latex

Definitions	DS(A), dstype(TypeNames; d; a), dseq(d;a), eqof(d), 1of(t), 2of(t), x. t(x), EqDecider(T), x:A. B(x), t  T
Lemmas	deq wf, pi2 wf, pi1 wf, eqof wf